ePMC

Benchmark
Model:speed-ind v.1 (CTMC)
Parameter(s)T = 2100
Property:change_state (prob-reach-time-bounded)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files speed-ind.prism --model-input-type prism --property-input-files speed-ind.props --property-input-names change_state --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const T=2100
Execution
Walltime:177.15648555755615s
Return code:0
Relative Error:1.4123045256958517e-08
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property change_state
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 8805 8804
build-model-states-explored 21261 12457
build-model-states-explored 35046 13785
build-model-states-explored 48657 13611
build-model-states-explored 62350 13693
build-model-states-explored 75977 13627
build-model-states-explored 89035 13057
build-model-states-explored 103200 14165
build-model-states-explored 116974 13774
build-model-states-explored 130393 13419
build-model-states-explored 143794 13401
build-model-states-explored 157477 13683
build-model-states-explored 169587 12109
build-model-states-explored 183966 14380
build-model-states-explored 197746 13780
build-model-states-explored 211130 13384
build-model-states-explored 224876 13746
build-model-states-explored 239013 14137
build-model-states-explored 252648 13635
build-model-states-explored 264326 11678
build-model-states-explored 277990 13664
build-model-states-explored 292189 14199
build-model-states-explored 306053 13864
build-model-states-explored 319410 13357
build-model-states-explored 330165 10755
build-model-states-explored 344530 14365
build-model-states-explored 358209 13679
build-model-states-explored 371858 13649
build-model-states-explored 385228 13370
build-model-states-explored 399550 14322
build-model-states-explored 413297 13747
build-model-states-explored 426991 13694
build-model-states-explored 440506 13515
build-model-states-explored 454640 14134
build-model-states-explored 468584 13943
build-model-states-explored 482332 13749
build-model-states-explored 495806 13474
build-model-states-explored 510037 14231
build-model-states-explored 523986 13949
build-model-states-explored 533954 9968
build-model-states-explored 547512 13558
build-model-states-explored 561885 14373
build-model-states-explored 575873 13988
build-model-states-explored 589358 13484
build-model-states-explored 603668 14311
build-model-states-explored 617793 14125
build-model-states-explored 631356 13563
build-model-states-explored 645724 14368
build-model-states-explored 654130 8406
build-model-states-explored 668082 13951
build-model-states-explored 682300 14219
build-model-states-explored 696589 14289
build-model-states-explored 710790 14201
build-model-states-explored 725322 14532
build-model-states-explored 739994 14672
build-model-done 743424 55
iterating-progress-bounded 47 6298 0.007462686567164179 1
iterating-progress-bounded 102 6298 0.016195617656398858 2
iterating-progress-bounded 157 6298 0.024928548745633536 3
iterating-progress-bounded 211 6298 0.0335026992696094 4
iterating-progress-bounded 266 6298 0.042235630358844076 5
iterating-progress-bounded 321 6298 0.05096856144807876 6
iterating-progress-bounded 376 6298 0.05970149253731343 7
iterating-progress-bounded 431 6298 0.06843442362654811 8
iterating-progress-bounded 485 6298 0.07700857415052398 9
iterating-progress-bounded 540 6298 0.08574150523975865 10
iterating-progress-bounded 595 6298 0.09447443632899333 11
iterating-progress-bounded 650 6298 0.103207367418228 12
iterating-progress-bounded 705 6298 0.11194029850746269 13
iterating-progress-bounded 759 6298 0.12051444903143856 14
iterating-progress-bounded 814 6298 0.12924738012067322 15
iterating-progress-bounded 869 6298 0.13798031120990792 16
iterating-progress-bounded 924 6298 0.1467132422991426 17
iterating-progress-bounded 978 6298 0.15528739282311846 18
iterating-progress-bounded 1032 6298 0.16386154334709432 19
iterating-progress-bounded 1087 6298 0.172594474436329 20
iterating-progress-bounded 1141 6298 0.18116862496030486 21
iterating-progress-bounded 1196 6298 0.18990155604953954 22
iterating-progress-bounded 1250 6298 0.1984757065735154 23
iterating-progress-bounded 1305 6298 0.20720863766275008 24
iterating-progress-bounded 1359 6298 0.21578278818672594 25
iterating-progress-bounded 1413 6298 0.2243569387107018 26
iterating-progress-bounded 1468 6298 0.23308986979993648 27
iterating-progress-bounded 1522 6298 0.24166402032391235 28
iterating-progress-bounded 1577 6298 0.25039695141314705 29
iterating-progress-bounded 1631 6298 0.2589711019371229 30
iterating-progress-bounded 1686 6298 0.2677040330263576 31
iterating-progress-bounded 1740 6298 0.27627818355033346 32
iterating-progress-bounded 1795 6298 0.28501111463956813 33
iterating-progress-bounded 1849 6298 0.293585265163544 34
iterating-progress-bounded 1904 6298 0.30231819625277867 35
iterating-progress-bounded 1958 6298 0.31089234677675454 36
iterating-progress-bounded 2013 6298 0.3196252778659892 37
iterating-progress-bounded 2067 6298 0.3281994283899651 38
iterating-progress-bounded 2122 6298 0.33693235947919975 39
iterating-progress-bounded 2176 6298 0.3455065100031756 40
iterating-progress-bounded 2231 6298 0.3542394410924103 41
iterating-progress-bounded 2285 6298 0.36281359161638616 42
iterating-progress-bounded 2340 6298 0.37154652270562083 43
iterating-progress-bounded 2394 6298 0.3801206732295967 44
iterating-progress-bounded 2449 6298 0.38885360431883137 45
iterating-progress-bounded 2503 6298 0.39742775484280723 46
iterating-progress-bounded 2558 6298 0.4061606859320419 47
iterating-progress-bounded 2612 6298 0.4147348364560178 48
iterating-progress-bounded 2667 6298 0.42346776754525245 49
iterating-progress-bounded 2721 6298 0.4320419180692283 50
iterating-progress-bounded 2776 6298 0.440774849158463 51
iterating-progress-bounded 2830 6298 0.44934899968243885 52
iterating-progress-bounded 2885 6298 0.45808193077167353 53
iterating-progress-bounded 2939 6298 0.4666560812956494 54
iterating-progress-bounded 2994 6298 0.47538901238488407 55
iterating-progress-bounded 3048 6298 0.48396316290885993 56
iterating-progress-bounded 3103 6298 0.4926960939980946 57
iterating-progress-bounded 3157 6298 0.5012702445220705 58
iterating-progress-bounded 3212 6298 0.5100031756113051 59
iterating-progress-bounded 3266 6298 0.5185773261352811 60
iterating-progress-bounded 3320 6298 0.5271514766592569 61
iterating-progress-bounded 3375 6298 0.5358844077484916 62
iterating-progress-bounded 3429 6298 0.5444585582724675 63
iterating-progress-bounded 3484 6298 0.5531914893617021 64
iterating-progress-bounded 3538 6298 0.561765639885678 65
iterating-progress-bounded 3593 6298 0.5704985709749126 66
iterating-progress-bounded 3647 6298 0.5790727214988886 67
iterating-progress-bounded 3702 6298 0.5878056525881232 68
iterating-progress-bounded 3756 6298 0.596379803112099 69
iterating-progress-bounded 3811 6298 0.6051127342013337 70
iterating-progress-bounded 3865 6298 0.6136868847253096 71
iterating-progress-bounded 3920 6298 0.6224198158145443 72
iterating-progress-bounded 3974 6298 0.6309939663385201 73
iterating-progress-bounded 4029 6298 0.6397268974277548 74
iterating-progress-bounded 4083 6298 0.6483010479517307 75
iterating-progress-bounded 4138 6298 0.6570339790409654 76
iterating-progress-bounded 4192 6298 0.6656081295649412 77
iterating-progress-bounded 4247 6298 0.674341060654176 78
iterating-progress-bounded 4301 6298 0.6829152111781518 79
iterating-progress-bounded 4356 6298 0.6916481422673865 80
iterating-progress-bounded 4410 6298 0.7002222927913624 81
iterating-progress-bounded 4465 6298 0.7089552238805971 82
iterating-progress-bounded 4519 6298 0.7175293744045729 83
iterating-progress-bounded 4574 6298 0.7262623054938075 84
iterating-progress-bounded 4628 6298 0.7348364560177835 85
iterating-progress-bounded 4683 6298 0.7435693871070181 86
iterating-progress-bounded 4737 6298 0.752143537630994 87
iterating-progress-bounded 4792 6298 0.7608764687202286 88
iterating-progress-bounded 4846 6298 0.7694506192442045 89
iterating-progress-bounded 4900 6298 0.7780247697681804 90
iterating-progress-bounded 4954 6298 0.7865989202921563 91
iterating-progress-bounded 5009 6298 0.795331851381391 92
iterating-progress-bounded 5063 6298 0.8039060019053668 93
iterating-progress-bounded 5117 6298 0.8124801524293427 94
iterating-progress-bounded 5172 6298 0.8212130835185774 95
iterating-progress-bounded 5226 6298 0.8297872340425532 96
iterating-progress-bounded 5281 6298 0.8385201651317878 97
iterating-progress-bounded 5335 6298 0.8470943156557638 98
iterating-progress-bounded 5390 6298 0.8558272467449984 99
iterating-progress-bounded 5444 6298 0.8644013972689742 100
iterating-progress-bounded 5499 6298 0.8731343283582089 101
iterating-progress-bounded 5553 6298 0.8817084788821848 102
iterating-progress-bounded 5608 6298 0.8904414099714195 103
iterating-progress-bounded 5662 6298 0.8990155604953953 104
iterating-progress-bounded 5717 6298 0.90774849158463 105
iterating-progress-bounded 5771 6298 0.9163226421086059 106
iterating-progress-bounded 5826 6298 0.9250555731978406 107
iterating-progress-bounded 5880 6298 0.9336297237218164 108
iterating-progress-bounded 5935 6298 0.9423626548110511 109
iterating-progress-bounded 5989 6298 0.950936805335027 110
iterating-progress-bounded 6044 6298 0.9596697364242617 111
iterating-progress-bounded 6098 6298 0.9682438869482375 112
iterating-progress-bounded 6153 6298 0.9769768180374722 113
iterating-progress-bounded 6207 6298 0.9855509685614481 114
iterating-progress-bounded 6262 6298 0.9942838996506828 115
model-checking-done 175
command-check-result-is 0.04229449867732711 change_state